Skip to content

support submodules in cryptol_load #2593

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 57 commits into from
Oct 19, 2025
Merged

support submodules in cryptol_load #2593

merged 57 commits into from
Oct 19, 2025

Conversation

@mtullsen
Copy link
Contributor

@mtullsen mtullsen commented Sep 10, 2025 •
edited
Loading

See Also

Notes re the implementation

  • The goal here is to common up (as much possible) the code from the currently working import implementation into the code for cryptol_load (and cryptol_extract).
  • A lot of the changes are refactorings to allow for the above "commoning up" (some of which were non-trivial, relying on arguments beyond syntactic rewriting).
  • During testing, a bug was discovered in import & load
    • privates in submodules were being silently ignored.
    • this was fixed, a large rewrite involved, see the code in CryptolSAWCore.CryptolEnv.computeNamingEnv

@mtullsen mtullsen self-assigned this Sep 10, 2025
This was referenced Sep 9, 2025
Closed
Merged
@mtullsen mtullsen force-pushed the tullsen/support-submodules-in-cryptol_load branch 4 times, most recently from 52b831f to 729af4c Compare September 19, 2025 21:25
@mtullsen mtullsen force-pushed the tullsen/support-submodules-in-cryptol_load branch 2 times, most recently from d80957b to 93fd2d8 Compare September 30, 2025 05:16
@mtullsen mtullsen force-pushed the tullsen/support-submodules-in-cryptol_load branch from 0ff5951 to a89ed12 Compare October 11, 2025 23:46
@mtullsen mtullsen marked this pull request as ready for review October 12, 2025 04:51
@RyanGlScott RyanGlScott mentioned this pull request Oct 13, 2025
Merged
RyanGlScott
RyanGlScott reviewed Oct 13, 2025
View reviewed changes
sauclovian-g
sauclovian-g reviewed Oct 14, 2025
View reviewed changes
mtullsen added 13 commits October 18, 2025 21:31
@mtullsen
refactor: new function loadAndTranslateModule, extracted from importM…
04585d2 
…odule function.

# Conflicts:
#	cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
@mtullsen
comments and whitespace
920a822
@mtullsen
refactor: move code for generating CryptolModule into mkCryptolModule
3a82d6a 
- See comments in mkCryptolModule that justify the refactor (i.e., that modEnv' == modEnv'')
@mtullsen
refactors
0ed7208
@mtullsen
improve fail message
6eadbea
@mtullsen
comments.
82f02a4
@mtullsen
refactor: fold loadAndTranslateModule
2f445b5
@mtullsen
comments, refactors
e88ed53
@mtullsen
refactor: make names more consistent
d5dad71 
- s/importModule/importCryptolModule/g;
@mtullsen
improve comments
bb89001
@mtullsen
comments, refactors (re-ordering, folding locatedUnknown, new mkImport)
86c6c53
@mtullsen
refactor (with dead code, thus no compile), in prep for ...
764eb6d
@mtullsen
generalize the internals of "CryptolModule" (as seen on command-line)…
1f33f04 
… and updating code to reflect this

- CryptolModule (as known at the command line) is generalized to ExtCryptolModule,
  - this allows for a module to be represented as EITHER
    - CryptolModule (2 namespaces), or
    - the name of a loaded module

- This allows for simpler and newly shared code
- This now should support submodules when we `cryptol_load`.
mtullsen added 24 commits October 18, 2025 21:31
@mtullsen
tweak F.cry test module
422242d
@mtullsen
add debugging code (temporarily)
660aa35
@mtullsen
refactor (modulo debug logging details); tweaking .cry tests
28c77db
@mtullsen
checkpoint (logging code shows proposed new code)
1479130
@mtullsen
refactor (turning logging messages into org outline)
b0127a7
@mtullsen
checkpoint
bea8b6e
@mtullsen
refactor, plus fixing nmsPr (based on nmsTopLevels)
e5516c2
@mtullsen
checkpoint: compiles
8f056b0
@mtullsen
checkpoint: many things working, publics in submodules now missing.
0e9e252
@mtullsen
refactor: renaming
a4ef330
@mtullsen
more logging, ensure it is off by default
7bcbab9
@mtullsen
comments
6928264
@mtullsen
fix computeNamingEnv
2137dd2 
Now working: full support of submodules, private, nominal types, and etc.
@mtullsen
Update tests (now that they pass).
9b66459
@mtullsen
refactor (with previous bump): move functions to deps/cryptol
c3265ba
@mtullsen
fixup the merge
0c8eb86 
this change was broken, but now is correct:
32556b1.. : cryptol-saw-core: Only import nominal types from non-parameterized modules
@mtullsen
whitespace, and elaborate comments
2137a1e
@mtullsen
Tweak the tests (defined correctly, more comments, all passing).
68b412d
@mtullsen
remove debugging code
5c331fa
@mtullsen
update doc/developer
0cc7170
@mtullsen
Update CHANGES.md with doc for submodules and changed cryptol_load be…
0594a50 
…havior.
@mtullsen
remove doc file, moved to Issue #2701.
ecb16d9
@mtullsen
refactors and add documentation
edd37dc 
based on code reviews by @RyanGIScott @sauclovian-g
@mtullsen
whitespace: follow existing whitespace/layout conventions more closely.
48dc42a
@mtullsen mtullsen force-pushed the tullsen/support-submodules-in-cryptol_load branch from 61c374d to 48dc42a Compare October 19, 2025 04:46
@mtullsen
Copy link
Contributor Author

Everything should be addressed @RyanGlScott @sauclovian-g.

@mtullsen mtullsen merged commit 0c192bd into master Oct 19, 2025
37 checks passed
@mtullsen mtullsen deleted the tullsen/support-submodules-in-cryptol_load branch October 19, 2025 20:09
@sauclovian-g sauclovian-g mentioned this pull request Oct 20, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sauclovian-g sauclovian-g sauclovian-g left review comments

@RyanGlScott RyanGlScott RyanGlScott approved these changes

@brianhuffman brianhuffman Awaiting requested review from brianhuffman

Assignees

@mtullsen mtullsen

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@mtullsen @RyanGlScott @sauclovian-g